add_nat_wf_com
12,41
postcript
pdf
It is a bad idea to make these usual wf
lemmas since often one mixes integer funs and
nat funs. (e.g.
n
:
,
i
:{0...
n
}. (-
i
)+
n
)
Sometime maybe should figure out systematic way of
dealing with
,
polymorphism
origin
n:
, i:{0...n}. (-i)+n 
)
,
polymorphismn:, i:{0...n}. (-i)+n )
, polymorphism